T:Type{i}, x:T, L:(T List), P:(TTprop{i':l}).
pairwise(x,y.P(x,y); cons(x; L))  (pairwise(x,y.P(x,y); L)  l_all(L; T; y.P(x,y))) 

latex

Definitions	x(s1,s2), t  T, int_seg(i; j), A, lelt(i; j; k), P  Q, A  B, P  Q, False, x:A. B(x), l_all(L; T; x.P(x)), prop{i:l}
Lemmas	select wf, length wf1, non neg length, length cons, select member, select cons tl sq, le wf